Search Results

Documents authored by Doukmak, Anna


Document
Short Paper
Towards Verifying the Bitcoin-S Library (Short Paper)

Authors: Ramon Boss, Kai Brünnler, and Anna Doukmak

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


Abstract
We try to verify properties of the Bitcoin-S library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since Bitcoin-S is not written in this fragment, we extract the relevant code from it and rewrite it until we arrive at code that we successfully verify. In that process we find and fix two bugs in Bitcoin-S.

Cite as

Ramon Boss, Kai Brünnler, and Anna Doukmak. Towards Verifying the Bitcoin-S Library (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 8:1-8:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{boss_et_al:OASIcs.FMBC.2020.8,
  author =	{Boss, Ramon and Br\"{u}nnler, Kai and Doukmak, Anna},
  title =	{{Towards Verifying the Bitcoin-S Library}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{8:1--8:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.8},
  URN =		{urn:nbn:de:0030-drops-134212},
  doi =		{10.4230/OASIcs.FMBC.2020.8},
  annote =	{Keywords: Bitcoin, Scala, Bitcoin-S, Stainless}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail